| Definitions |  T, effect-p-realizable, decl-type{i:l}(ds; x), es-locl(es; e; e'), alle-at(es; i; e.P(e)), Knd, frame-p-realizable,  A, guard(T), sq_type(T),  e@i.P(e), x:A. B(x), A c B, @i locl(a) occurs once, es-init-state(es; i), init-p-realizable, Rplus-right(x1), Rplus-left(x1), Rplus?(x1),  b, True, Y, reduce(f; k; as), ff, Rlist(L), pre-p-realizable, discrete-pre-p-realizable, es-realizer(p), t.2, t.1, P Q, tt, if b then t else f fi , top, normal-type{i:l}(T), es-state-ap(s; x), onceR{$a:ut2, $done:ut2}(i),   x. t(x), P   Q, prop{i:l}, t  T, mkid{$x:ut2}, Id,  x:A. B(x),  b, effect-p(es; i; ds; k; T; x; f), wellfounded{i:l}(A; x,y.R(x;y)), @i only L affect x:T, decidable(P), es-state-after(es; e), P  Q, existse-ge(es; e; e'.P(e')), es-state-when(es; e), es-dtype(es; i; x; T), P  Q, P Q, init-p(es; i; T; x; v), @i Precondition for a(Outcome(p)) P discrete state(ds), Unit, False, R-realizes{i:l}(R; es.P(es)), decl-state(ds), es-real{i:l}(es.P(es)), es_realizer{i:l}, x(s), Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rsends(ds; knd; T; l; dt; g), Rsframe(lnk; tag; L), Rnone, Rplus(left; right), Rframe(loc; T; x; L), Reffect(loc; ds; knd; T; x; f), Rinit(loc; T; x; v), Rpre(loc; ds; a; p; P),  |
| Lemmas | es-axioms, decidable l member, es-pred-locl, squash wf, fpf-cap-single1, btrue wf, p-outcome wf, effect-p wf, lnk wf, ldst wf, isrcv wf, natural number wf p-outcome, es-after-pred2, es-pred wf, bool sq, es-locl wf, es-locl-iff, es-loc-pred, es-when wf, es-causl wf, es-locl-wellfnd, member singleton, l member wf, frame-p-es-frame, frame-p wf, normal-type wf, decidable equal Kind, locl wf, init-p-implies, es-E wf, es-first wf, es-dtype wf, es-when-first-discrete, decidable equal bool, change-since-init, not wf, es-vartype wf, es-after wf, assert wf, not functionality wrt iff, es-kind wf, es-loc wf, es-le-loc, Id sq, not-assert, es-initially wf, assert of bnot, es-dds-single, R-sub-plus-right3, bfalse wf, init-p wf, R-sub-plus-left, decl-type wf, IdLnk wf, Knd wf, rationals wf, unit wf, es realizer wf, false wf, true wf, R-sub-implies, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, bnot wf, fpf-single wf3, unit-fps wf, discrete-pre-p wf, es-real wf, normal-ds wf, decl-state wf, fpf wf, finite-prob-space wf, bool-inhabited, bool wf, normal-ds-single, Id wf, R-consistent wf, event system wf, once-p wf, implies-es-real, onceR feasible, onceR wf |